Nuprl Lemma : atom-free-es-kindtype
0,22
postcript
pdf
es
:ES,
i
:Id,
k
:Knd. AtomFree(Type;kindtype(
i
;
k
))
latex
Definitions
islocal(
k
)
,
isrcv(
k
)
,
x
:
A
B
(
x
)
,
left
+
right
,
Knd
,
t
T
,
x
:
A
.
B
(
x
)
,
tag(
k
)
,
lnk(
k
)
,
act(
k
)
,
Id
,
P
&
Q
,
es-V(
es
)
,
es-M(
es
)
,
kindtype(
i
;
k
)
,
ES
,
x
:
A
B
(
x
)
,
f
(
a
)
,
kindcase(
k
;
a
.
f
(
a
);
l
,
t
.
g
(
l
;
t
) )
,
Type
,
AtomFree(
T
;
x
)
Lemmas
event
system
wf
,
Knd
wf
,
Id
wf
origin
es:ES, i:Id, k:Knd. AtomFree(Type;kindtype(i;k)) es:ES, i:Id, k:Knd. AtomFree(Type;kindtype(i;k)) 
B(x)
Tx:A. B(x)
B(x)